In this section, we discuss the results of verifying the OCL contraints definedin Section \ref{subsec:FormulationOCLConsts} using the verification prototype.We show how the verification prototype was able to uncover bugs in theGM-to-AUTOSAR transformation that were fixed and re-verified. We also describethe results of a study to determine the performance of the used verificationapproach.